\section{Subtyping}

\subsubsection{Object Subtyping}
Subtyping is never implicit. In most cases you need specify the
\textit{codomain} of the type coercion, sometimes you also need
specify \textit{domain} of the type coercion.

Narrowing coercions is not allowed in \textit{Ocaml}. Subtyping and
inheritance are not related. \textit{Inheritance} is a
\textit{syntactic relation} between classes while subtyping is a
semantic relation between types.

\begin{ocamlcode}
let f c = (c :> point);;
val f : #point -> point = <fun>  
\end{ocamlcode}
\captionof{listing}{Coercion example}

\begin{ocamlcode}
class type c1 = object method m : c1  end;;
class type c1 = object method m : c1 end

class type c2 = object ('a) method m : 'a  end;;
class type c2 = object ('a) method m : 'a end

let to_c1 x = (x:>c1);;
val to_c1 : < m : #c1; .. > -> c1 = <fun>

let to_c2 x = (x:>c2);;
val to_c2 : #c2 -> c2 = <fun>
\end{ocamlcode}
\captionof{listing}{Subtlety of Subtyping Class}

In \textit{to\_c1}, c1 was expanded and unrolled twice to obtain
\textit{< <m:c1; ..>; .. >} (remember \textit{\#c1 = <m : c1;..> })
without introducing recursion, in \textit{to\_c2}, \textit{\#c2} was
equal to \textit{<m:'a; ...> as 'a}
You should know that \textit{class type c1} and \textit{class type c2}
was subtly different.


A common problem is that when one tries to define a coercion to a
class \textit{c} while defining class \textit{c}.


\begin{ocamlcode}
class c = object
    method m = 1
  end
  and d = object(self)
  inherit c
  method n = 2
  method as_c = (self :> c)
  end;;
\end{ocamlcode}
\captionof{listing}{Self coerce}
Here \textit{self} tried to coerce to a object type, but the object
type is not closed yet.  Here is the error message


\begin{bashcode}
Error: This expression cannot be coerced to type c = < m : int >; it has type
         < as_c : c; m : int; n : int; .. >
       but is here used with type c
       Self type cannot be unified with a closed object type
     \end{bashcode}

However, ocaml take it as a special case that coercing self to its
current class is fine.     

\begin{ocamlcode}
let all_c = ref [];;
val all_c : '_a list ref = {contents = []}
# class c (m:int) = object(self)
    method m = m
    initializer all_c := (self:>c)::!all_c
end     
;;
        class c : int -> object method m : int end  
\end{ocamlcode}
\captionof{listing}{Coercing to itself}

An interesting example is that you can do object lookup 
as follows:

\begin{ocamlcode}
let rec lookup_obj obj = function [] -> raise Not_found
| obj' :: l -> if (obj :> < > ) = (obj' :> < > ) then obj'
else lookup_obj obj l;;
val lookup_obj : < .. > -> (< .. > as 'a) list -> 'a = <fun>
let lookup_c obj = lookup_obj obj !all_c
\end{ocamlcode}
\captionof{listing}{Object lookup}

The object equality considers \textit{reference equality} only.

\subsubsection{Solution to Self coercion}

You can predefine the abbreviation using a class type

\begin{ocamlcode}
class type c' = object method m : int end ;;
class type c' = object method m : int end
# class c: c' = object method m = 1 end
  and d = object (self)
   inherit c
   method as_c = (self:>c')
   end;;
        class c : c'
and d : object method as_c : c' method m : int end  
\end{ocamlcode}
\captionof{listing}{Solution to Self coercion}

\subsection{Polymorphic Variant Subtyping}

\begin{ocamlcode}
  let f x = (x:[`A] :> [`A | `B ])
\end{ocamlcode}
\captionof{listing}{basic subtyping}

\begin{ocamlcode}
  let f x = (x:[`A] *[`B] :> [`A | `C] * [`B | `D]);;
  val f : [ `A ] * [ `B ] -> [ `A | `C ] * [ `B | `D ] = <fun>
\end{ocamlcode}
\captionof{listing}{tuple subtyping}

\begin{ocamlcode}
  let f x = (x:[`A|`B ] -> [`A ] :> [`A] -> [`A | `B]);;
  val f : ([ `A | `B ] -> [ `A ]) -> [ `A ] -> [ `A | `B ] = <fun>
\end{ocamlcode}
\captionof{listing}{function subtyping}

\begin{ocamlcode}
  let f x = (x: [`A] list :> [`A|`B] list);;
  val f : [ `A ] list -> [ `A | `B ] list = <fun>
\end{ocamlcode}
\captionof{listing}{predefined variance relation}
The compiler already knows the type constructor \textit{list} is
co-variant.

OCaml can infer the variance relation in most case, for
example

\begin{ocamlcode}
  type (+'a, +'b) t = 'a * 'b
  type (-'a, -'b) t = 'a -> 'b 
\end{ocamlcode}

Here the variance notation is not necessary, if you annotate it, the
compiler will checkt its correctness. The problem lies when you
encapsulate  the type definition, if you don't annotate it, the
compiler will not keep track of \textit{those constraints} for you,
finally you will lose those contraints. So, you should tell the
compiler to keep track it for me.

\begin{ocamlcode}
  module M : sig
    type (+'a, +'b)t 
    end = struct
    type ('a, 'b)t = 'a * 'b
  end
\end{ocamlcode}

Now the following code will check

\begin{ocamlcode}
let f x = ( x : ([`A], [`B]) M.t :> ([`A|`C], [`B|`D]) M.t);;
val f : ([ `A ], [ `B ]) M.t -> ([ `A | `C ], [ `B | `D ]) M.t = <fun>  
\end{ocamlcode}

Another interesting bit is when \textit{'a t} is co-variant,


\begin{ocamlcode}
  module M : sig
  type +'a t
  val embed : 'a -> 'a t 
 end = struct
  type 'a t = 'a
  let embed x = x
 end ;;
\end{ocamlcode}

\begin{ocamlcode}
  M.embed [] :: 'a list t 
\end{ocamlcode}
Otherwise, it will be \textit{'\_a list M.t}


\subsection{Private type subtyping}
\label{sec:priv-type-subtyp}

Private type stand between abstract type and concrete types. You can
\textit{coerce} your private type back to the concrete type
(zero-performance), but backward is \textbf{not allowed}.

For ordinary private type, you can still do pattern match, print the
result in toplevel, and debugger. You \textit{can not do coercion for abstract
types}.

Even for parameterized type(like container) coercion, you can still do
the coercion pretty fast(optimization), and some parameterized
types(not containers) can still do such coercions.  Since ocaml does
not provide ad-hoc polymorphism, or type functions like Haskell, its
soundness is pretty straight-forward.

\inputminted[fontsize=\scriptsize,linenos=true ]{ocaml}{code/types/priv.ml}
\captionof{listing}{Private type subtyping}

So private type is kinda like \textit{newtype} in Haskell, but with
little cost. Since \textit{private type} suports coercion directly,
you can use \textit{coercion} to encode some policy

\begin{ocamlcode}
  type readonly = private int 
  module Ref : sig
    type  +'a t
    .... 
  end = struct
  end
  
  let x = Ref.create 3
  let y = (x:> readonly Ref.t)
\end{ocamlcode}

Another thing to notice is that compiler can break the private
boundary to do optimizations, which means compiler can make use of the
fact that it knows its concrete type.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../master.tex"
%%% End: 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../master"
%%% End: 
